Serveur d'exploration sur les relations entre la France et l'Australie

Attention, ce site est en cours de développement !
Attention, site généré par des moyens informatiques à partir de corpus bruts.
Les informations ne sont donc pas validées.

Modular State Spaces for Prioritised Petri Nets

Identifieur interne : 006385 ( Main/Exploration ); précédent : 006384; suivant : 006386

Modular State Spaces for Prioritised Petri Nets

Auteurs : Charles Lakos [Australie] ; Laure Petrucci [France]

Source :

RBID : ISTEX:995167D6676261A6F0BCE4AD7ABA26DA817D358B

English descriptors

Abstract

Abstract: Verification of complex systems specification often encounters the so-called state space explosion problem, which prevents exhaustive model-checking in many practical cases. Many techniques have been developed to counter this problem by reducing the state space, either by retaining a smaller number of relevant states, or by using a smart representation. Among the latter, modular state spaces [CP00, LP04] have turned out to be an efficient analysis technique in many cases [Pet05]. When the system uses a priority mechanism (e.g. timed systems [LP07]), there is increased coupling between the modules — preemption between modules can occur, thus disabling local events. This paper shows that the approach is still applicable even when considering dynamic priorities, i.e. priorities depending both on the transition and the current marking.

Url:
DOI: 10.1007/978-3-642-21292-5_8


Affiliations:


Links toward previous steps (curation, corpus...)


Le document en format XML

<record>
<TEI wicri:istexFullTextTei="biblStruct">
<teiHeader>
<fileDesc>
<titleStmt>
<title xml:lang="en">Modular State Spaces for Prioritised Petri Nets</title>
<author>
<name sortKey="Lakos, Charles" sort="Lakos, Charles" uniqKey="Lakos C" first="Charles" last="Lakos">Charles Lakos</name>
</author>
<author>
<name sortKey="Petrucci, Laure" sort="Petrucci, Laure" uniqKey="Petrucci L" first="Laure" last="Petrucci">Laure Petrucci</name>
</author>
</titleStmt>
<publicationStmt>
<idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:995167D6676261A6F0BCE4AD7ABA26DA817D358B</idno>
<date when="2011" year="2011">2011</date>
<idno type="doi">10.1007/978-3-642-21292-5_8</idno>
<idno type="url">https://api.istex.fr/document/995167D6676261A6F0BCE4AD7ABA26DA817D358B/fulltext/pdf</idno>
<idno type="wicri:Area/Istex/Corpus">001D15</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001D15</idno>
<idno type="wicri:Area/Istex/Curation">001D15</idno>
<idno type="wicri:Area/Istex/Checkpoint">000804</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000804</idno>
<idno type="wicri:doubleKey">0302-9743:2011:Lakos C:modular:state:spaces</idno>
<idno type="wicri:Area/Main/Merge">006761</idno>
<idno type="wicri:Area/Main/Curation">006385</idno>
<idno type="wicri:Area/Main/Exploration">006385</idno>
</publicationStmt>
<sourceDesc>
<biblStruct>
<analytic>
<title level="a" type="main" xml:lang="en">Modular State Spaces for Prioritised Petri Nets</title>
<author>
<name sortKey="Lakos, Charles" sort="Lakos, Charles" uniqKey="Lakos C" first="Charles" last="Lakos">Charles Lakos</name>
<affiliation wicri:level="1">
<country xml:lang="fr">Australie</country>
<wicri:regionArea>University of Adelaide, 5005, Adelaide, SA</wicri:regionArea>
<wicri:noRegion>SA</wicri:noRegion>
</affiliation>
<affiliation wicri:level="1">
<country wicri:rule="url">Australie</country>
</affiliation>
</author>
<author>
<name sortKey="Petrucci, Laure" sort="Petrucci, Laure" uniqKey="Petrucci L" first="Laure" last="Petrucci">Laure Petrucci</name>
<affiliation wicri:level="1">
<country xml:lang="fr">France</country>
<wicri:regionArea>LIPN, CNRS UMR 7030, Université Paris XIII, 99, avenue Jean-Baptiste Clément, F-93430, Villetaneuse</wicri:regionArea>
<wicri:noRegion>93430, Villetaneuse</wicri:noRegion>
<wicri:noRegion>Villetaneuse</wicri:noRegion>
</affiliation>
<affiliation wicri:level="1">
<country wicri:rule="url">France</country>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series>
<title level="s">Lecture Notes in Computer Science</title>
<imprint>
<date>2011</date>
</imprint>
<idno type="ISSN">0302-9743</idno>
<idno type="eISSN">1611-3349</idno>
<idno type="ISSN">0302-9743</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt>
<idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc>
<textClass>
<keywords scheme="KwdEn" xml:lang="en">
<term>Algorithm</term>
<term>Composite sequence</term>
<term>Consistent priority function</term>
<term>Constituent transitions</term>
<term>Dynamic priorities</term>
<term>Fieldbus protocol</term>
<term>Forall</term>
<term>Global priority function</term>
<term>Gure</term>
<term>Higher priority</term>
<term>Individual modules</term>
<term>Intermediate synchronisation points</term>
<term>Internal activity</term>
<term>Internal transitions</term>
<term>Lakos</term>
<term>Local component</term>
<term>Local sequence</term>
<term>Local sequences</term>
<term>Local state space</term>
<term>Local state spaces</term>
<term>Local transition</term>
<term>Local transitions</term>
<term>Maximum priority</term>
<term>Minimum priority</term>
<term>Modular</term>
<term>Modular analysis</term>
<term>Modular nets</term>
<term>Modular petri</term>
<term>Modular petri nets</term>
<term>Modular state space</term>
<term>Modular state space exploration</term>
<term>Modular state spaces</term>
<term>Module</term>
<term>Node</term>
<term>Nodes reachable</term>
<term>Nogn</term>
<term>Nogn nogn</term>
<term>Nogu</term>
<term>Normal message</term>
<term>Normal messages</term>
<term>Other hand</term>
<term>Other words</term>
<term>Petri</term>
<term>Petri nets</term>
<term>Petrucci</term>
<term>Prioritised</term>
<term>Prioritised petri</term>
<term>Prioritised petri nets</term>
<term>Priority</term>
<term>Priority function</term>
<term>Priority scheme</term>
<term>Reachable</term>
<term>Ring rule</term>
<term>Ring transition</term>
<term>Same priority</term>
<term>State space</term>
<term>State space explosion problem</term>
<term>State spaces</term>
<term>Synchronisation</term>
<term>Synchronisation graph</term>
<term>Synchronisation point</term>
<term>Synchronisation transitions</term>
<term>Timing constraints</term>
<term>Transition group</term>
<term>Transition groups</term>
<term>Urgent message</term>
<term>Urgent messages</term>
</keywords>
<keywords scheme="Teeft" xml:lang="en">
<term>Algorithm</term>
<term>Composite sequence</term>
<term>Consistent priority function</term>
<term>Constituent transitions</term>
<term>Dynamic priorities</term>
<term>Fieldbus protocol</term>
<term>Forall</term>
<term>Global priority function</term>
<term>Gure</term>
<term>Higher priority</term>
<term>Individual modules</term>
<term>Intermediate synchronisation points</term>
<term>Internal activity</term>
<term>Internal transitions</term>
<term>Lakos</term>
<term>Local component</term>
<term>Local sequence</term>
<term>Local sequences</term>
<term>Local state space</term>
<term>Local state spaces</term>
<term>Local transition</term>
<term>Local transitions</term>
<term>Maximum priority</term>
<term>Minimum priority</term>
<term>Modular</term>
<term>Modular analysis</term>
<term>Modular nets</term>
<term>Modular petri</term>
<term>Modular petri nets</term>
<term>Modular state space</term>
<term>Modular state space exploration</term>
<term>Modular state spaces</term>
<term>Module</term>
<term>Node</term>
<term>Nodes reachable</term>
<term>Nogn</term>
<term>Nogn nogn</term>
<term>Nogu</term>
<term>Normal message</term>
<term>Normal messages</term>
<term>Other hand</term>
<term>Other words</term>
<term>Petri</term>
<term>Petri nets</term>
<term>Petrucci</term>
<term>Prioritised</term>
<term>Prioritised petri</term>
<term>Prioritised petri nets</term>
<term>Priority</term>
<term>Priority function</term>
<term>Priority scheme</term>
<term>Reachable</term>
<term>Ring rule</term>
<term>Ring transition</term>
<term>Same priority</term>
<term>State space</term>
<term>State space explosion problem</term>
<term>State spaces</term>
<term>Synchronisation</term>
<term>Synchronisation graph</term>
<term>Synchronisation point</term>
<term>Synchronisation transitions</term>
<term>Timing constraints</term>
<term>Transition group</term>
<term>Transition groups</term>
<term>Urgent message</term>
<term>Urgent messages</term>
</keywords>
</textClass>
<langUsage>
<language ident="en">en</language>
</langUsage>
</profileDesc>
</teiHeader>
<front>
<div type="abstract" xml:lang="en">Abstract: Verification of complex systems specification often encounters the so-called state space explosion problem, which prevents exhaustive model-checking in many practical cases. Many techniques have been developed to counter this problem by reducing the state space, either by retaining a smaller number of relevant states, or by using a smart representation. Among the latter, modular state spaces [CP00, LP04] have turned out to be an efficient analysis technique in many cases [Pet05]. When the system uses a priority mechanism (e.g. timed systems [LP07]), there is increased coupling between the modules — preemption between modules can occur, thus disabling local events. This paper shows that the approach is still applicable even when considering dynamic priorities, i.e. priorities depending both on the transition and the current marking.</div>
</front>
</TEI>
<affiliations>
<list>
<country>
<li>Australie</li>
<li>France</li>
</country>
</list>
<tree>
<country name="Australie">
<noRegion>
<name sortKey="Lakos, Charles" sort="Lakos, Charles" uniqKey="Lakos C" first="Charles" last="Lakos">Charles Lakos</name>
</noRegion>
<name sortKey="Lakos, Charles" sort="Lakos, Charles" uniqKey="Lakos C" first="Charles" last="Lakos">Charles Lakos</name>
</country>
<country name="France">
<noRegion>
<name sortKey="Petrucci, Laure" sort="Petrucci, Laure" uniqKey="Petrucci L" first="Laure" last="Petrucci">Laure Petrucci</name>
</noRegion>
<name sortKey="Petrucci, Laure" sort="Petrucci, Laure" uniqKey="Petrucci L" first="Laure" last="Petrucci">Laure Petrucci</name>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Asie/explor/AustralieFrV1/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 006385 | SxmlIndent | more

Ou

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 006385 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Asie
   |area=    AustralieFrV1
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     ISTEX:995167D6676261A6F0BCE4AD7ABA26DA817D358B
   |texte=   Modular State Spaces for Prioritised Petri Nets
}}

Wicri

This area was generated with Dilib version V0.6.33.
Data generation: Tue Dec 5 10:43:12 2017. Site generation: Tue Mar 5 14:07:20 2024